H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.47000000000000003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule FiniteMap

((sizeFM :: FiniteMap b a -> Int) :: FiniteMap b a -> Int)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

sizeFM :: FiniteMap b a -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch _ _ size _ _)	=	size

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule FiniteMap

((sizeFM :: FiniteMap b a -> Int) :: FiniteMap b a -> Int)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

sizeFM :: FiniteMap a b -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch vw vx size vy vz)	=	size

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule FiniteMap

((sizeFM :: FiniteMap a b -> Int) :: FiniteMap a b -> Int)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

sizeFM :: FiniteMap b a -> Int

sizeFM	EmptyFM	=	0
sizeFM	(Branch vw vx size vy vz)	=	size

module Maybe where

import qualified FiniteMap
import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule FiniteMap

(sizeFM :: FiniteMap b a -> Int)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

sizeFM :: FiniteMap a b -> Int

sizeFM	EmptyFM	=	Pos Zero
sizeFM	(Branch vw vx size vy vz)	=	size

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sizeFM",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sizeFM ww3",fontsize=16,color="burlywood",shape="triangle"];8[label="ww3/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];3 -> 8[label="",style="solid", color="burlywood", weight=9];
8 -> 4[label="",style="solid", color="burlywood", weight=3];
9[label="ww3/Branch ww30 ww31 ww32 ww33 ww34",fontsize=10,color="white",style="solid",shape="box"];3 -> 9[label="",style="solid", color="burlywood", weight=9];
9 -> 5[label="",style="solid", color="burlywood", weight=3];
4[label="sizeFM EmptyFM",fontsize=16,color="black",shape="box"];4 -> 6[label="",style="solid", color="black", weight=3];
5[label="sizeFM (Branch ww30 ww31 ww32 ww33 ww34)",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="Pos Zero",fontsize=16,color="green",shape="box"];7[label="ww32",fontsize=16,color="green",shape="box"];}